A:Type, eq:EqDecider(A), B:(AType), f:a:A fp B(a), x:A, v:B(x).
f || x : v  (x  dom(f)  v = f(x)) 

latex

Definitions	t  T, Top, x(s), P  Q, x:A. B(x), x. t(x), a:A fp B(a), x : v, x  dom(f), b, Prop, P & Q, f(x), f || g, EqDecider(T), P  Q, P  Q
Lemmas	subtype rel self, fpf-single-dom-sq, deq property, fpf-compatible wf, fpf-ap wf, fpf wf, deq wf, assert wf, fpf-dom wf, fpf-single wf, top wf, fpf-trivial-subtype-top